(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #x044479e555b49cb0) #xfffffffffffffffe))
(constraint (= (f #x7443308b9d5b8686) #x0e88661173ab70d1))
(constraint (= (f #x663d8a0a5d897e01) #x0cc7b1414bb12fc1))
(constraint (= (f #x11e895366c2e42d2) #xfffffffffffffffe))
(constraint (= (f #xe553d1d60dd06e15) #xffffffffffffffff))
(constraint (= (f #xb54e3a804d9a3796) #xfffffffffffffffe))
(constraint (= (f #x02ac4ae709e25dde) #xfffffffffffffffe))
(constraint (= (f #x53a7062dd83a29d8) #xfffffffffffffffe))
(constraint (= (f #x20e7598e78122439) #xffffffffffffffff))
(constraint (= (f #xd6e1179b4d465d8a) #xfffffffffffffffe))
(constraint (= (f #x01b7c3e754e77ed0) #x0036f87cea9cefdb))
(constraint (= (f #xb9e92e54d37cedc9) #xffffffffffffffff))
(constraint (= (f #xe8297433d564884a) #xfffffffffffffffe))
(constraint (= (f #x2e89c4aea712854e) #xfffffffffffffffe))
(constraint (= (f #x4eb03cd2e64203ec) #xfffffffffffffffe))
(constraint (= (f #x3235e6cbc5943958) #xfffffffffffffffe))
(constraint (= (f #x9069c75ee0ab2cbe) #x020d38ebdc156598))
(constraint (= (f #xc8e9e939ee5ee37a) #xfffffffffffffffe))
(constraint (= (f #xab99cadca4dc522e) #xfffffffffffffffe))
(constraint (= (f #xd4bec5ebe49ac8e1) #xffffffffffffffff))
(constraint (= (f #x6a77b2744e68a064) #xfffffffffffffffe))
(constraint (= (f #xb3849a897e430381) #x067093512fc86071))
(constraint (= (f #xd0ab163d5202aace) #xfffffffffffffffe))
(constraint (= (f #x2693009bebb99e2e) #x04d260137d7733c6))
(constraint (= (f #x1de1ec231e3d6e06) #x03bc3d8463c7adc1))
(constraint (= (f #xe1db335aa98c9ae9) #xffffffffffffffff))
(constraint (= (f #x4aa77668e2e90d77) #x0954eecd1c5d21af))
(constraint (= (f #x6eec429414b2944a) #xfffffffffffffffe))
(constraint (= (f #x6138ec217259d0b0) #x0c271d842e4b3a17))
(constraint (= (f #x015889ed901be195) #x002b113db2037c33))
(constraint (= (f #x2873a7ea323e7cd6) #xfffffffffffffffe))
(constraint (= (f #x769e9659c2cda939) #x0ed3d2cb3859b528))
(constraint (= (f #x920abc0a4c6be091) #x02415781498d7c13))
(constraint (= (f #x2e698c8d5daeb742) #xfffffffffffffffe))
(constraint (= (f #xac91e7c4855024c6) #xfffffffffffffffe))
(constraint (= (f #xa98e863c5918ea46) #xfffffffffffffffe))
(constraint (= (f #x80762e83a017cbec) #x000ec5d07402f97e))
(constraint (= (f #x6c912e2bca417cac) #x0d9225c579482f96))
(constraint (= (f #xc75305ad00bead4a) #xfffffffffffffffe))
(constraint (= (f #x46a03dc511c7ee5b) #x08d407b8a238fdcc))
(constraint (= (f #xa5e8bd25c79dc81e) #x04bd17a4b8f3b904))
(constraint (= (f #xbb4b82139d1b1d52) #x0769704273a363ab))
(constraint (= (f #x77d6ad735e5c1784) #xfffffffffffffffe))
(constraint (= (f #xe6b7e35855e7ee73) #x0cd6fc6b0abcfdcf))
(constraint (= (f #xdacee71e030e9790) #xfffffffffffffffe))
(constraint (= (f #xe2d48665ab8de5ee) #x0c5a90ccb571bcbe))
(constraint (= (f #x68eb01b7083e1098) #xfffffffffffffffe))
(constraint (= (f #x95c72379ea891d18) #x02b8e46f3d5123a4))
(constraint (= (f #x63967e15e2407314) #xfffffffffffffffe))
(constraint (= (f #xe3b294592d07c555) #x0c76528b25a0f8ab))
(constraint (= (f #x6e3c46a84021ee74) #x0dc788d508043dcf))
(constraint (= (f #x2d720b5e2666eeeb) #xffffffffffffffff))
(constraint (= (f #x3464abc87008420b) #xffffffffffffffff))
(constraint (= (f #x2a65de96e326b8ab) #xffffffffffffffff))
(constraint (= (f #xeae2e09c55b6845b) #xffffffffffffffff))
(constraint (= (f #x34470308d9262a97) #xffffffffffffffff))
(constraint (= (f #xec8a1e00e3ce29ec) #xfffffffffffffffe))
(constraint (= (f #x81029b274c1258ed) #xffffffffffffffff))
(constraint (= (f #xe397b796116b9207) #x0c72f6f2c22d7241))
(constraint (= (f #x9c5ede71c42d4154) #x038bdbce3885a82b))
(constraint (= (f #x1aced6371860a819) #xffffffffffffffff))
(constraint (= (f #x014142ee09835428) #x0028285dc1306a86))
(constraint (= (f #xa7bb183d234408b5) #xffffffffffffffff))
(constraint (= (f #xb4ec6282a2386173) #xffffffffffffffff))
(constraint (= (f #xe9a028208495c15a) #x0d3405041092b82c))
(constraint (= (f #xea66659ec74de966) #x0d4cccb3d8e9bd2d))
(constraint (= (f #x80bba50ec87ace16) #xfffffffffffffffe))
(constraint (= (f #x638ba79805eabd15) #xffffffffffffffff))
(constraint (= (f #x0ae837dd196eba32) #xfffffffffffffffe))
(constraint (= (f #x6d94e2c8d253ee08) #x0db29c591a4a7dc2))
(constraint (= (f #xe75b8668b2222e2d) #xffffffffffffffff))
(constraint (= (f #xc815d86e3cdd2e32) #x0902bb0dc79ba5c7))
(constraint (= (f #x1b7a1398664ae2ce) #xfffffffffffffffe))
(constraint (= (f #x14502017d24e6d52) #xfffffffffffffffe))
(constraint (= (f #xea41e45c78e48cd3) #xffffffffffffffff))
(constraint (= (f #xc482c4e932cecae3) #xffffffffffffffff))
(constraint (= (f #x4056b7ea18cbc294) #x080ad6fd43197853))
(constraint (= (f #x929a0ece5316eeeb) #xffffffffffffffff))
(constraint (= (f #xda46ddb156465e8c) #xfffffffffffffffe))
(constraint (= (f #xa89de2b9aea84189) #xffffffffffffffff))
(constraint (= (f #xad5e09d07ee7836e) #x05abc13a0fdcf06e))
(constraint (= (f #xee3ee9721c77788c) #x0dc7dd2e438eef12))
(constraint (= (f #x069eaa5212580bb2) #xfffffffffffffffe))
(constraint (= (f #x8cc884ceee9a2e11) #xffffffffffffffff))
(constraint (= (f #x321820d5603ce4cd) #xffffffffffffffff))
(constraint (= (f #xe53e3776ab010796) #x0ca7c6eed56020f3))
(constraint (= (f #x28d43c39167d869e) #x051a878722cfb0d4))
(constraint (= (f #x61eb04130d6ea757) #xffffffffffffffff))
(constraint (= (f #xa0ac200e6585b86b) #x04158401ccb0b70e))
(constraint (= (f #x8ee20eb1e6dbaeec) #x01dc41d63cdb75de))
(constraint (= (f #x8de49207c38bd699) #x01bc9240f8717ad4))
(constraint (= (f #x2eb179383a3b90ea) #x05d62f270747721e))
(constraint (= (f #x590bdce68875e4e4) #x0b217b9cd10ebc9d))
(constraint (= (f #x3e775e6e5acd6759) #x07ceebcdcb59acec))
(constraint (= (f #x13b9b86e3d504715) #xffffffffffffffff))
(constraint (= (f #x0ea61ccb7185619d) #x01d4c3996e30ac34))
(constraint (= (f #x466548838c08a47a) #xfffffffffffffffe))
(constraint (= (f #xb4e148ae7c662e0a) #xfffffffffffffffe))
(constraint (= (f #x6e34cd477b666beb) #xffffffffffffffff))
(constraint (= (f #xec409ea78113e512) #x0d8813d4f0227ca3))
(check-synth)
